Theorem jca2 512

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 511	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  rr19.28v  3655  preddowncl  6345  ssimaex  6987  onfununi  8371  oaordex  8588  domtriord  9161  findcard3  9319  findcard3OLD  9320  unfilem1  9344  fodomfibOLD  9373  inf0  9664  inf3lem3  9673  tcel  9788  fidomtri2  10037  alephval3  10153  zorn2lem6  10544  fodomb  10569  eqreznegel  12970  iserodd  16837  cshwsiun  17102  txcn  23621  ssfg  23867  fclsnei  24014  eldmgm  27050  fnrelpredd  34926  cvmlift2lem10  35140  relcnveq3  38019  iss2  38042  elrelscnveq3  38189  jca3  38554  prjspreln0  42263  omabs2  42998  tfsconcatrn  43008  rfovcnvf1od  43671  mnuop3d  43945