Theorem jctild 529

Description: Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.)

Hypotheses

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

Assertion

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

Proof of Theorem jctild

Step	Hyp	Ref	Expression
1		jctild.2	. . 3 ⊢ (𝜑 → 𝜃)
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3		jctild.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	jcad 516	1 ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anc2li  559  equvini  2467  2reu1  3806  ordunidif  6223  isofrlem  7094  dfwe2  7502  orduniorsuc  7551  poxp  7834  fnse  7839  ssenen  8727  dffi3  8942  fpwwe2lem12  10116  zmulcl  12084  rpneg  12476  rexuz3  14770  cau3lem  14776  climrlim2  14966  o1rlimmul  15037  iseralt  15103  gcdzeq  15968  isprm3  16094  vdwnnlem2  16402  ablfaclem3  19292  epttop  21724  lmcnp  22019  dfconn2  22134  txcnp  22335  cmphaushmeo  22515  isfild  22573  cnpflf2  22715  flimfnfcls  22743  alexsubALT  22766  fgcfil  23986  bcthlem5  24043  ivthlem2  24167  ivthlem3  24168  dvfsumrlim  24745  plypf1  24923  axeuclidlem  26870  usgr2wlkneq  27659  wwlksnredwwlkn0  27796  wwlksnextwrd  27797  clwlkclwwlklem2a1  27891  lnon0  28695  hstles  30128  mdsl1i  30218  atcveq0  30245  atcvat4i  30294  cdjreui  30329  issgon  31624  connpconn  32727  tfisg  33316  frpoinsg  33342  frmin  33348  noetalem1  33543  outsideofrflx  34014  isbasisrelowllem1  35088  isbasisrelowllem2  35089  poimirlem3  35376  poimirlem29  35402  poimir  35406  heicant  35408  equivtotbnd  35532  ismtybndlem  35560  cvrat4  37055  linepsubN  37364  pmapsub  37380  osumcllem4N  37571  pexmidlem1N  37582  dochexmidlem1  39072  harval3  40663  clcnvlem  40742  iccpartimp  44362  sbgoldbwt  44722  sbgoldbst  44723  elsetrecslem  45726