Theorem jca2 513

Description: Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 12-Oct-2010.)

Hypotheses

Ref	Expression
jca2.1	⊢ (𝜑 → (𝜓 → 𝜒))
jca2.2	⊢ (𝜓 → 𝜃)

Assertion

Ref	Expression
jca2	⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Proof of Theorem jca2

Step	Hyp	Ref	Expression
1		jca2.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		jca2.2	. . 3 ⊢ (𝜓 → 𝜃)
3	2	a1i 11	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4	1, 3	jcad 512	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  rr19.28v  3681  preddowncl  6364  ssimaex  7007  onfununi  8397  oaordex  8614  domtriord  9189  findcard3  9346  findcard3OLD  9347  unfilem1  9371  fodomfibOLD  9399  inf0  9690  inf3lem3  9699  tcel  9814  fidomtri2  10063  alephval3  10179  zorn2lem6  10570  fodomb  10595  eqreznegel  12999  iserodd  16882  cshwsiun  17147  txcn  23655  ssfg  23901  fclsnei  24048  eldmgm  27083  fnrelpredd  35065  cvmlift2lem10  35280  relcnveq3  38277  iss2  38300  elrelscnveq3  38447  jca3  38812  prjspreln0  42564  omabs2  43294  tfsconcatrn  43304  rfovcnvf1od  43966  mnuop3d  44240