Theorem 3expib 1140

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expib	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Proof of Theorem 3expib

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1137	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 416	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anidm12  1446  mob  3678  dfss2  3920  eqbrrdva  5853  f1resrcmplf1dlem  7275  f1oiso2  7357  frxp  8128  onfununi  8334  smoel2  8356  smoiso2  8362  3ecoptocl  8813  ssfi  9171  f1domfi  9179  rex2dom  9227  fodomfib  9302  dffi2  9397  elfiun  9404  dif1card  10017  infxpenlem  10020  cfeq0  10262  cfsuc  10263  cfflb  10265  cfslb2n  10274  cofsmo  10275  domtriomlem  10448  axdc3lem4  10459  axdc4lem  10461  ttukey2g  10522  tskxpss  10785  grudomon  10830  elnpi  11001  dedekind  11401  nn0n0n1ge2b  12601  fzind  12723  suprzcl2  12991  icoshft  13530  fzen  13599  hashgt23el  14493  hashfundm  14511  hashbclem  14521  seqcoll  14533  relexpsucl  15108  relexpsucr  15109  relexpfld  15126  shftuz  15146  mulgcd  16644  algcvga  16675  lcmneg  16699  ressbas  17334  resseqnbas  17340  ressress  17345  psss  18674  tsrlemax  18680  isnmgm  18740  gsummgmpropd  18789  issgrpd  18838  iscmnd  19927  ring1ne0  20447  unitmulclb  20528  isdrngd  20937  isdrngdOLD  20939  abvn0b  21008  issrngd  21027  rmodislmodlem  21119  rmodislmod  21120  isphld  21873  mpfaddcl  22335  mpfmulcl  22336  pf1addcl  22584  pf1mulcl  22585  fitop  23131  hausnei2  23584  ordtt1  23610  locfincmp  23758  basqtop  23943  filfi  24091  fgcl  24110  neifil  24112  filuni  24117  cnextcn  24299  prdsmet  24602  blssps  24656  blss  24657  metcnp3  24772  hlhil  25677  volsup2  25839  sincosq1sgn  26743  sincosq2sgn  26744  sincosq3sgn  26745  sincosq4sgn  26746  sinq12ge0  26753  bcmono  27521  n0cutlt  28632  bdayfin  28760  iswlkg  30081  usgrwwlks2on  30434  umgrwwlks2on  30435  clwlkclwwlkfo  30487  loop1cycl  30631  umgr2cycllem  30633  umgr2cycl  30634  3cyclfrgrrn1  30773  grpodivf  31027  ipf  31202  shintcli  31818  spanuni  32033  adjadj  32425  unopadj2  32427  hmopadj  32428  hmopbdoptHIL  32477  resvsca  33780  resvlem  33781  submateq  34327  esumcocn  34598  bnj1379  35347  bnj571  35423  bnj594  35429  bnj580  35430  bnj600  35436  bnj1189  35526  bnj1321  35544  bnj1384  35549  trssfir1om  35629  fineqvinfep  35659  trssfir1omregs  35670  karddom  35695  kardsdom  35696  kardexen  35697  onvfowev  35721  cplgredgex  35727  cusgr3cyclex  35733  acycgr2v  35737  cusgracyclt3v  35743  climuzcnv  36258  fness  36976  cgsex2gd  37897  bj-idreseq  37922  bj-imdiridlem  37945  neificl  38511  metf1o  38513  isismty  38559  ismtybndlem  38564  ablo4pnp  38638  divrngcl  38715  keridl  38790  prnc  38825  lsmsatcv  39891  llncvrlpln2  40438  lplncvrlvol2  40496  linepsubN  40633  pmapsub  40649  dalawlem10  40761  dalawlem13  40764  dalawlem14  40765  dalaw  40767  diaf11N  41930  dibf11N  42042  ismrcd1  43551  ismrcd2  43552  mzpincl  43587  mzpadd  43591  mzpmul  43592  pellfundge  43731  imasgim  43949  sqrtcval  44489  stoweidlem2  46838  stoweidlem17  46853  imaelsetpreimafv  48303  opnneir  49841  i0oii  49854  io1ii  49855