Theorem ancrd 542

Description: Deduction conjoining antecedent to right of consequent in nested implication. (Contributed by NM, 15-Aug-1994.) (Proof shortened by Wolf Lammen, 1-Nov-2012.)

Hypothesis

Ref	Expression
ancrd.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
ancrd	⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜓)))

Proof of Theorem ancrd

Step	Hyp	Ref	Expression
1		ancrd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		idd 24	. 2 ⊢ (𝜑 → (𝜓 → 𝜓))
3	1, 2	jcad 503	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜓)))

Syntax hints:   → wi 4   ∧ wa 383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 198  df-an 384

This theorem is referenced by:  impac  543  equvinva  2120  reupick  4069  prel12OLD  4525  reusv2lem3  5014  ssrelrn  5465  ssrnres  5724  funmo  6058  funssres  6084  dffo4  6535  dffo5  6536  dfwe2  7149  ordpwsuc  7183  ordunisuc2  7212  dfom2  7235  nnsuc  7250  nnaordex  7893  wdom2d  8662  iundom2g  9585  fzospliti  12730  rexuz3  14318  qredeq  15599  prmdvdsfz  15644  dirge  17465  lssssr  19185  lssssrOLD  19186  lpigen  19491  psgnodpm  20169  neiptopnei  21177  metustexhalf  22601  dyadmbllem  23607  3cyclfrgrrn2  27490  atexch  29597  ordtconnlem1  30327  isbasisrelowllem1  33557  isbasisrelowllem2  33558  phpreu  33743  poimirlem26  33785  sstotbnd3  33923  eqlkr3  34925  dihatexv  37163  dvh3dim2  37273  neik0pk1imk0  38885  pm14.123b  39166  ordpss  39193  climreeq  40369  reuan  41725  2reu1  41731